$\vdash$ ($\lambda$$A$,$a$,$z$. $a$ $\in$ $A$) $\in$ $A$:Type$\rightarrow$$A$$\rightarrow$($\downarrow$True)$\rightarrow$Type